Report for preprocessed.c

Generated on 2018-06-07 17:14:21 by CPAchecker 1.7

Matches in value-assignements (V): {{numOfValueMatches}}

Matches in edge-description: {{numOfDescriptionMatches}}

-V-
{{line.desc}}
1
/* service_maxrgb_cpu.c */  
2
  
3
/* service_maxrgb.h */  
4
  
5
#ifndef __SERVICE_MAXRGB_H__  
6
#define __SERVICE_MAXRGB_H__  
7
  
8
/* service_plugin.h */  
9
  
10
#ifndef __SERVICE_PLUGIN_H__  
11
#define __SERVICE_PLUGIN_H__  
12
  
13
#include <stdint.h>  
14
  
15
#define QuantumRange UINT16_MAX  
16
  
17
typedef uint16_t Quantum;  
18
  
19
typedef struct __PixelPacket__ {  
20
	Quantum blue;  
21
	Quantum green;  
22
	Quantum red;  
23
	Quantum opacity;  
24
} PixelPacket;  
25
  
26
typedef struct __Image__ {  
27
	PixelPacket *image;  
28
	int32_t rows;  
29
	int32_t columns;  
30
	int64_t j_arr;  
31
} Image;  
32
  
33
void run_service(char resource, void *handler_gpu, Image **target_images, int32_t *target_images_size, Image *source_images, int32_t source_images_size, double *params, int32_t *status_code);  
34
  
35
void get_service_ids(char ***id_strings, int32_t *id_strings_size);  
36
void get_service_info(char ***info_strings, int32_t *info_strings_size);  
37
void get_service_params(char ***param_strings, int32_t *param_strings_size);  
38
void get_service_resources(char ***resource_strings, int32_t *resource_strings_size);  
39
int32_t get_number_of_input_images(void);  
40
int32_t get_number_of_output_images(void);  
41
  
42
#endif /* __SERVICE_PLUGIN_H__ */  
43
/* common.h */  
44
  
45
#ifndef __COMMON_H__  
46
#define __COMMON_H__  
47
  
48
#include <stdio.h>  
49
  
50
void malloc_copy_string_array(char ***target_array, char **source_array, int32_t array_size);  
51
void free_string_array(char ***array, int32_t array_size);  
52
  
53
#endif /* __COMMON_H__ */  
54
  
55
#include <stdio.h>  
56
  
57
int32_t run_service_maxrgb_scpu(PixelPacket *pixpack_target, PixelPacket *pixpack_source, int32_t rows, int32_t columns, int32_t mode);  
58
int32_t run_service_maxrgb_cpu(PixelPacket *pixpack_target, PixelPacket *pixpack_source, int32_t rows, int32_t columns, int32_t mode);  
59
int32_t run_service_maxrgb_gpu(PixelPacket *pixpack_target, PixelPacket *pixpack_source, int32_t rows, int32_t columns, int32_t mode);  
60
int32_t run_service_maxrgb_fpga(PixelPacket *pixpack_target, PixelPacket *pixpack_source, int32_t rows, int32_t columns, int32_t mode);  
61
  
62
// internal maxfile interface(s)  
63
void run_service_max_maxrgb(uint16_t *dataOut, uint16_t *dataIn, uint32_t picSize, uint32_t mode);  
64
	  
65
#endif /* __SERVICE_MAXRGB_H__ */  
66
  
67
int32_t run_service_maxrgb_cpu(PixelPacket *pixpack_target, PixelPacket *pixpack_source, int32_t rows, int32_t columns, int32_t mode) {  
68
	int32_t i, j, pos;  
69
  
70
	/**  
71
	  * Modes:  
72
	  * 1: maxRGB  
73
	  * 2: minRGB  
74
	  * 3: max increase  
75
	  * 4: min erase  
76
	**/  
77
  
78
	if ((mode == 1) || (mode == 3)) {  
79
		#pragma omp parallel  
80
		{  
81
			#pragma omp for private(j, pos)  
82
			for (i = 0; i < rows; ++i) {  
83
				for (j = 0; j < columns; ++j) {  
84
					pos = i * columns + j;  
85
  
86
					//check if color is grey  
87
					if ((pixpack_source[pos].red == pixpack_source[pos].green) && (pixpack_source[pos].red == pixpack_source[pos].blue)) {  
88
						pixpack_target[pos].red	  = pixpack_source[pos].red;  
89
						pixpack_target[pos].green = pixpack_source[pos].green;  
90
						pixpack_target[pos].blue  = pixpack_source[pos].blue;  
91
						continue;  
92
					}  
93
  
94
  
95
					uint16_t *maxPtr;  
96
					maxPtr = &pixpack_source[pos].blue;  
97
					uint16_t *colorPtr;  
98
					colorPtr = &pixpack_source[pos].blue;  
99
					int8_t c;  
100
  
101
					for (c = 1; c < 3; c++) {  
102
						colorPtr++;  
103
						if (*colorPtr > *maxPtr)  
104
							maxPtr = colorPtr;  
105
					}  
106
  
107
					uint16_t *colorPtrSource;  
108
					colorPtrSource = &pixpack_source[pos].blue;  
109
					uint16_t *colorPtrTarget;  
110
					colorPtrTarget = &pixpack_target[pos].blue;  
111
  
112
					switch (mode) {  
113
						case 1:  
114
							for (c = 0; c < 3; c++) {  
115
								if (colorPtrSource == maxPtr)  
116
									*colorPtrTarget = *colorPtrSource;  
117
								else  
118
									*colorPtrTarget = 0;  
119
  
120
								colorPtrSource++;  
121
								colorPtrTarget++;  
122
							}  
123
							break;  
124
						case 3:  
125
							for (c = 0; c < 3; c++) {  
126
								if (colorPtrSource == maxPtr)  
127
									*colorPtrTarget = 65535;  
128
								else  
129
									*colorPtrTarget = *colorPtrSource;  
130
  
131
								colorPtrSource++;  
132
								colorPtrTarget++;  
133
							}  
134
					}  
135
				}  
136
			}  
137
		}  
138
	} else if ((mode == 2) || (mode == 4)) {  
139
		#pragma omp parallel  
140
		{  
141
			#pragma omp for private(j, pos)  
142
			for (i = 0; i < rows; ++i) {  
143
				for (j = 0; j < columns; ++j) {  
144
					pos = i * columns + j;  
145
  
146
					//check if color is grey  
147
					if ((pixpack_source[pos].red == pixpack_source[pos].green) && (pixpack_source[pos].red == pixpack_source[pos].blue)) {  
148
						pixpack_target[pos].red	  = pixpack_source[pos].red;  
149
						pixpack_target[pos].green = pixpack_source[pos].green;  
150
						pixpack_target[pos].blue  = pixpack_source[pos].blue;  
151
						continue;  
152
					}  
153
  
154
  
155
					uint16_t *minPtr;  
156
					minPtr = &pixpack_source[pos].blue;  
157
					uint16_t *colorPtr;  
158
					colorPtr = &pixpack_source[pos].blue;  
159
					int8_t c;  
160
  
161
					for (c = 1; c < 3; c++) {  
162
						colorPtr++;  
163
						if (*colorPtr < *minPtr)  
164
							minPtr = colorPtr;  
165
					}  
166
  
167
					uint16_t *colorPtrSource;  
168
					colorPtrSource = &pixpack_source[pos].blue;  
169
					uint16_t *colorPtrTarget;  
170
					colorPtrTarget = &pixpack_target[pos].blue;  
171
  
172
					switch (mode) {  
173
						case 2:  
174
							for (c = 0; c < 3; c++) {  
175
								if (colorPtrSource == minPtr)  
176
									*colorPtrTarget = *colorPtrSource;  
177
								else  
178
									*colorPtrTarget = 0;  
179
  
180
								colorPtrSource++;  
181
								colorPtrTarget++;  
182
							}  
183
							break;  
184
						case 4:  
185
							for (c = 0; c < 3; c++) {  
186
								if (colorPtrSource == minPtr)  
187
									*colorPtrTarget = 0;  
188
								else  
189
									*colorPtrTarget = *colorPtrSource;  
190
  
191
								colorPtrSource++;  
192
								colorPtrTarget++;  
193
							}  
194
					}  
195
				}  
196
			}  
197
		}  
198
	}  
199
	return 0;  
200
}  
2018-06-07 17:03:15:512	INFO	ResourceLimitChecker.fromConfiguration	Using the following resource limits: CPU-time limit of 900s

2018-06-07 17:03:15:793	INFO	CPAchecker.run	CPAchecker 1.7 (Java HotSpot(TM) 64-Bit Server VM 1.8.0_91) started

2018-06-07 17:03:19:170	WARNING	ARGCPA:FormulaManagerView.<init>	Using unsound approximation of ints with unbounded integers and floats with unbounded integers for encoding program semantics.

2018-06-07 17:03:19:279	INFO	CPAchecker.runAlgorithm	Starting analysis ...

2018-06-07 17:13:55:854	WARNING	ShutdownNotifier.shutdownIfNecessary	Warning: Analysis interrupted (The JVM is shutting down, probably because Ctrl+C was pressed.)

2018-06-07 17:13:55:859	SEVERE	ProofGenerator.generateProof	Proof cannot be generated because checked property not known to be true.

2018-06-07 17:14:09:925	WARNING	StatisticsUtils.writeOutputFiles	Writing output files from org.sosy_lab.cpachecker.cpa.arg.ARGStatistics took    14.039s.

    

AutomatonAnalysis (AssertionAutomaton) statistics
-------------------------------------------------
Number of states:                                  1
Total time for successor computation:                  1.173s
  Time for transition matches:                         0.507s
  Time for transition assertions:                      0.000s
  Time for transition actions:                         0.000s
Automaton transfers with branching:                0
Automaton transfer successors:                        59461 (count: 59461, min: 1, max: 1, avg: 1.00) [1 x 59461]

AutomatonAnalysis (ErrorLabelAutomaton) statistics
--------------------------------------------------
Number of states:                                  1
Total time for successor computation:                  0.523s
  Time for transition matches:                         0.198s
  Time for transition assertions:                      0.000s
  Time for transition actions:                         0.000s
Automaton transfers with branching:                0
Automaton transfer successors:                        59461 (count: 59461, min: 1, max: 1, avg: 1.00) [1 x 59461]

AutomatonAnalysis (TerminatingFunctions) statistics
---------------------------------------------------
Number of states:                                  1
Total time for successor computation:                  0.513s
  Time for transition matches:                         0.169s
  Time for transition assertions:                      0.000s
  Time for transition actions:                         0.000s
Automaton transfers with branching:                0
Automaton transfer successors:                        59461 (count: 59461, min: 1, max: 1, avg: 1.00) [1 x 59461]

CPA algorithm statistics
------------------------
Number of iterations:            52056
Max size of waitlist:            6
Average size of waitlist:        5
Number of computed successors:   59461
Max successors for one state:    2
Number of times merged:          0
Number of times stopped:         7401
Number of times breaked:         0

Total time for CPA algorithm:       636.558s (Max:   636.558s)
  Time for choose from waitlist:      0.284s
  Time for precision adjustment:      1.027s
  Time for transfer relation:         5.504s
  Time for merge operator:          388.203s
  Time for stop operator:           238.075s
  Time for adding to reached set:     0.899s

CPAchecker general statistics
-----------------------------
Number of program locations:     399
Number of CFA edges:             426
Number of relevant variables:    18
Number of functions:             1
Number of loops:                 10
Size of reached set:             52060
  Number of reached locations:   258 (65%)
    Avg states per location:     201
    Max states per location:     7401 (at node N92)
  Number of reached functions:   1 (100%)
  Number of partitions:          258
    Avg size of partitions:      201
    Max size of partitions:      7401 (with key [N92 (before line 142), Function run_service_maxrgb_cpu called from node N1, stack depth 1 [2974f221], stack [run_service_maxrgb_cpu]])
  Number of target states:       0
  Size of final wait list        5

Time for analysis setup:          3.470s
  Time for loading CPAs:          1.271s
  Time for loading parser:        0.607s
  Time for CFA construction:      1.479s
    Time for parsing file(s):     0.530s
    Time for AST to CFA:          0.351s
    Time for CFA sanity check:    0.055s
    Time for post-processing:     0.326s
      Time for var class.:        0.209s
        Time for collecting variables:                 0.060s
        Time for solving dependencies:                 0.001s
        Time for building hierarchy:                   0.000s
        Time for building classification:              0.109s
        Time for exporting data:                       0.016s
    Time for CFA export:          0.220s
Time for Analysis:              636.571s
CPU time for analysis:          648.730s
Total time for CPAchecker:      640.045s
Total CPU time for CPAchecker:  653.390s
Time for statistics:             14.288s

Time for Garbage Collector:       6.011s (in 1105 runs)
Garbage Collector(s) used:    PS MarkSweep, PS Scavenge
Used heap memory:                473MB (   451 MiB) max;    226MB (   215 MiB) avg;    621MB (   592 MiB) peak
Used non-heap memory:             32MB (    31 MiB) max;     30MB (    29 MiB) avg;     38MB (    36 MiB) peak
Used in PS Old Gen pool:          55MB (    52 MiB) max;     40MB (    38 MiB) avg;    162MB (   154 MiB) peak
Allocated heap memory:           485MB (   463 MiB) max;    423MB (   404 MiB) avg
Allocated non-heap memory:        34MB (    33 MiB) max;     34MB (    33 MiB) avg
Total process virtual memory:   3760MB (  3585 MiB) max;   3759MB (  3585 MiB) avg

    
analysis.entryFunction = run_service_maxrgb_cpu
analysis.programNames = preprocessed.c
analysis.traversal.order = DFS
ARGCPA.cpa = cpa.composite.CompositeCPA
CompositeCPA.cpas = cpa.location.LocationCPA, cpa.callstack.CallstackCPA, cpa.sign.SignCPA, cpa.interval.IntervalAnalysisCPA
coverage.enabled = false
cpa = cpa.PropertyChecker.PropertyCheckerCPA
cpa.callstack.domain = FLATPCC
cpa.callstack.skipRecursion = true
cpa.predicate.encodeBitvectorAs = INTEGER
cpa.predicate.encodeFloatAs = INTEGER
cpa.propertychecker.className = NoTargetStateChecker
limits.time.cpu = 900s
log.level = INFO
parser.usePreprocessor = true
pcc.proofFile = arg.proof
pcc.proofgen.doPCC = true
pcc.storeConfig = true
pcc.strategy = arg.ARG_CPAStrategy
PropertyCheckerCPA.cpa = cpa.arg.ARGCPA
solver.solver = SMTInterpol
specification = config/specification/default.spc
statistics.memory = true